E:Type, eq:EqDecider(E), T:(IdIdType), V:(KndIdType),
info:(E((:Id  Id) + (:(:IdLnk  E)  Id))), pred?:(E(?E)), val:(e:EV(kind(e),loc(e))), when,
after:(x:Ide:ET(loc(e),x)), time:(E), p:SESAxioms{i:l}(E;T;pred?;info;when;after;time).
ESAxioms{i:l}(E;T;l,tg. V(rcv(l,tg),destination(l));e.loc(e);e.kind(e);val;when;after;time;l,e.
sends(eq;IdLnkDeq;pred?;info;val;p.1;e;l);e.sender(e);e.index(eq;IdLnkDeq;pred?;info;p.1;e);e.
first(e);e.pred(e);e,e'. e < e') 

latex

Definitions

ESAxioms{i:l}(E;T;M;loc;kind;val;when;after;time;sends;sender;index;first;pred;causl), x:A  B(x), P & Q, SESAxioms{i:l}(E;T;pred?;info;when;after;time), Id, SWellFounded(R(x;y)), t  T, x:A. B(x), x.A(x), P  Q, x,y. t(x;y), Type, EqDecider(T), x:AB(x), Knd, IdLnk, left + right, Unit, loc(e), kind(e), f(a), , e < e', pred(e), s = t, first(e), b, A, A c B, WellFnd{i}(A;x,y.R(x;y)), pred!(e;e'), Void, P  Q, {T}, False, , sender(e), rcv?(e), P  Q, R^*, Dec(P), x. t(x), x f y, (i = j), rel_exp(T;R;n), A  B, a < b, {x:A| B(x)} , , , x:A. B(x), #$n, , inr x , True, <a, b>, R^+, R1 => R2, P  Q, Trans(T;x,y.E(x;y)), SQType(T), s ~ t, , n+m, b, , n - m, inl x , isrcv(k), msg(l;t;v), Msg(M), sends(dE;dL;pred?;info;val;p;e;l), l[i], ecase1(e;info;i.f(i);l,e'.g(l;e')), rcv(l,tg), locl(a), tag(k), lnk(k), destination(l), IdLnkDeq, receives(dE;dL;pred?;info;p;e;l), rcv-from-on(dE;dL;info;e;l;r), ||as||, i  j < k, index(dE;dL;pred?;info;p;r), link(e), {i..j}, T, S  T, suptype(S; T), rmsg(info;val;e), type List, i  j , eqof(d), (x  l), sends-bound(p;e;l), eventlist(pred?;e), mu(f), rtag(info;e), source(l), [], Msg_sub(l;M), t.1, x before y  l, index(L;x), x:A.B(x), Top

Lemmas

index-property1, sends wf, length-map, l before l index, l before filter, l before eventlist, strongwellfounded wf, l index wf, member receives, l before l index le, decidable le, squash wf, Msg sub wf, no-member-sq-nil, lsrc wf, rel plus implies, implies functionality wrt iff, strong-sends-bound-property, sends-bound-property, member eventlist, member filter, eventlist wf, sends-bound wf, l member wf, exists functionality wrt iff, deq property, mu-bound-property+, non neg length, eqof wf, select wf, subtype rel self, assert-rcv-from-on, map select, Msg wf, rmsg wf, index wf, int seg wf, link wf, length wf1, rcv-from-on wf, receives wf, idlnk-deq wf, msg wf, rcv wf, ldst wf, lnk wf, tagof wf, nat wf, isrcv wf, rel plus wf, bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, rel exp add, rel-rel-plus, wellfounded wf, rel plus strongwellfounded, rel exp monotone, nat plus inc, decidable int equal, rel plus trans, rel plus monotone, cless wf, pred-total, rel star transitivity, rel rel star, false wf, true wf, it wf, le wf, rel exp wf, rel star wf, decidable assert, rcv? wf, sender wf, wellfounded functionality wrt implies, not wf, assert wf, first wf, pred wf, SESAxioms wf, rationals wf, kind wf, loc wf, unit wf, IdLnk wf, Knd wf, deq wf, strongwf-implies, pred! wf, Id wf